$\forall$${\it es}$:ES, ${\it Cmd}$:Type, ${\it Sys}$:AbsInterface(chain\_sys(${\it Cmd}$)), $e$:E.
\\[0ex]Dec(($\uparrow$($e$ $\in_{b}$ ${\it Sys}$)) c$\wedge$ ($\uparrow$csinput?(${\it Sys}$($e$))))